$\forall$${\it es}$:event\_system\{i:l\}, $i$,$x$:Id, $s_{1}$,$s_{2}$:es\_state(${\it es}$; $i$).
\\[0ex]es{-}x{-}equiv(${\it es}$; $i$; $x$; $s_{1}$; $s_{2}$) $\in$ prop\{i:l\}